\begin{tabbing}
$\forall$$i$:Id, $L$:Id List, $k$:Knd.
\\[0ex]@$i$: $k$ affects only members of $L$ 
\\[0ex]realizes ${\it es}$.
\\[0ex]$\forall$$e$@$i$.
\\[0ex]kind($e$) $=$ $k$
\\[0ex]$\Rightarrow$ (\=$\forall$$x$:Id.\+
\\[0ex]($\neg$($x$ after $e$) $=$ ($x$ when $e$) $\in$ vartype($i$;$x$) $\Rightarrow$ ($x$ $\in$ $L$))
\\[0ex]\& ($\neg$($x$ $\in$ $L$) $\Rightarrow$ ($x$ after $e$) $=$ ($x$ when $e$) $\in$ vartype($i$;$x$)))
\-
\end{tabbing}